rcvs from e on l = L
== (e':E. (e'  L)  isrcv(e') & lnk(e') = l & sender(e') = e)
== & (e1, e2:E. e1 before e2  L  (e1 <loc e2)) 

latex

---

clarification:

es-rcv-from(es;e;l;L)
== (e':es-E(es).
== ((e'  L  es-E(es))
== (
== (es-isrcv(es; e') & es-lnk(es; e') = l  IdLnk & es-sender(es; e') = e  es-E(es))
== & (e1:es-E(es), e2:es-E(es). e1 before e2  L  es-E(es)  es-locl(es; e1; e2)) 

latex

Definitions	P  Q, (x  l), A & B, b, isrcv(e), P & Q, IdLnk, lnk(e), sender(e), x:A. B(x), P  Q, x before y  l, E, (e <loc e')
FDL editor aliases	es-rcv-from